\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $x$:Id, $T$:Type, ${\it ks}$:(Knd List),\+
\\[0ex]${\it tr}$:($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$)\} $\rightarrow$decl{-}state(${\it ds}$)$\rightarrow$ma{-}valtype(${\it da}$; $k$)$\rightarrow$$T$$\rightarrow$$T$).
\-\\[0ex]fpf{-}compatible(Id; $x$.Type; id{-}deq; ${\it ds}$; fpf{-}single($x$; $T$))
\\[0ex]$\Rightarrow$ \=($\forall$$k$:Knd. \+
\\[0ex]($\uparrow$fpf{-}dom(Kind{-}deq; $k$; R{-}da(R{-}state{-}var($i$; ${\it ds}$; ${\it da}$; $x$; $T$; ${\it ks}$; ${\it tr}$); $i$))) $\Rightarrow$ ($k$ $\in$ ${\it ks}$))
\-
\end{tabbing}